/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.transform;

import alloy.ast.ASTDepthFirstReplacer;
import alloy.ast.BinaryFormula;
import alloy.ast.ElemFormula;
import alloy.ast.ElemIntFormula;
import alloy.ast.EmptyFormula;
import alloy.ast.Formula;
import alloy.ast.FormulaSeq;
import alloy.ast.Formulas;
import alloy.ast.ImplicationFormula;
import alloy.ast.LogicOp;
import alloy.ast.NegFormula;
import alloy.ast.Node;
import alloy.ast.QuantifiedExpr;
import alloy.ast.QuantifiedFormula;
import alloy.ast.Quantifier;

/**
   <p>Performs a partial conversion of a formula to negation normal form (NNF).  Converting
   to NNF facilitates skolemization by moving negations inward, changing not all x | F(x) to
   some x | not F(x), and not some x | F(x) to all x | not F(x).  Complete conversion to NNF
   is not performed (iff and if-then-else nodes are untouched) to make sharing of subformulas
   easier to detect during translation.

   <p>This visitor assumes that
   all desugarings necessary before translation have been completed,
   and should be applied to a formula associated with a command.
*/

public class NNFVisitor extends ASTDepthFirstReplacer {

    /** count of number of negations seen up until this point */
    private int _negCount = 0;

    /** whether we are skolemizing inside universal quantifiers.  this
        affects how aggressive we are in pushing negations in when inside
        a universal quantifier */
    private boolean _skolemInsideUniv;

    public NNFVisitor(boolean skolemInsideUniv_) {
        _skolemInsideUniv = skolemInsideUniv_;
    }
    
    public Object visit(NegFormula negFormula_) {
        // first, increment the negation count
        _negCount++;
        
        // then, visit the negated formula, which
        // will be converted taking the current
        // negation into consideration
        Formula formula = negFormula_.getFormula();
        formula = (Formula)formula.applyReturnVisitor(this);
        
        // replace negFormula_ with the converted
        // version of the negated formula
        // NOTE: we don't need to make a copy here
        // since formula is a child of negFormula_
        // so there is no danger of a replacement
        // containing the original node
        formula.annotateReplacing("", negFormula_);
        // finally, decrement the negation count
        _negCount--;
        return formula;
    }

    public Object visit(FormulaSeq formulaSeq_) {
        // make sure formula sequence is non-empty
        if (!formulaSeq_.getFormulas().isLeaf()) {
            Formula replacement = null;
            Formulas formulas = formulaSeq_.getFormulas();
            for (int i = 0; i < formulas.numChildren(); i++) {
                // convert current formula                
                Formula curFormula = (Formula)formulas.childAt(i).applyReturnVisitor(this);
                if (negateFormula()) {
                    // using DeMorgan's law,
                    // ! (f1 && f2 && ... && fn) goes to
                    // !f1 || !f2 || ... || !fn
                    if (replacement == null) {
                        replacement = curFormula;
                    } else {
                        replacement = new BinaryFormula(replacement, LogicOp.OR, curFormula);
                    }
                }
                formulas.setChild(i, curFormula);
            }
            if (negateFormula()) {
                // replace original sequence
                replacement.annotateReplacing("", formulaSeq_);
                return replacement;
            }
        } else { // empty FormulaSeq
            if (negateFormula()) {
            	NegFormula nf = new NegFormula((Formula)formulaSeq_.copy());
            	nf.annotateReplacing("", formulaSeq_);
            	return nf;
            }
        }
        return formulaSeq_;
    }

    public Object visit(BinaryFormula binFormula_) {
        Formula left = binFormula_.getLeft();
        Formula right = binFormula_.getRight();
        
        LogicOp op = binFormula_.getOp();
        if (op.equals(LogicOp.AND) || op.equals(LogicOp.OR)) {
            // convert left and right formulas
            left = (Formula)left.applyReturnVisitor(this);
            right = (Formula)right.applyReturnVisitor(this);
            if (negateFormula()) {
                // using DeMorgan's law,
                // ! (f1 && f2) goes to
                // !f1 || !f2 and
                // ! (f1 || f2) goes to
                // !f1 && !f2
                LogicOp replOp = (op.equals(LogicOp.AND)) ? LogicOp.OR : LogicOp.AND;
                BinaryFormula bf = new BinaryFormula(left, replOp, right);
                bf.annotateReplacing("", binFormula_);
                return bf;
            } else {
            	// update original binary formula
            	binFormula_.setLeft(left);
            	binFormula_.setRight(right);
            	return binFormula_;
            }
        }
        else /*if (op.equals(LogicOp.IFF))*/ {
            return absorbNegation(binFormula_);
        }
    }

    public Object visit(ElemFormula elemFormula_) {
        return absorbNegation(elemFormula_);
    }

    public Object visit(ElemIntFormula elemIntFormula_) {
        return absorbNegation(elemIntFormula_);
    }

    public Object visit(ImplicationFormula implFormula_) {
        if (implFormula_.getElseFormula() instanceof EmptyFormula) {
            // transform f1 -> f2 to !f1 || f2 and then convert
            // the resulting formula
            Formula replacement = new BinaryFormula(new NegFormula(implFormula_.getIfFormula()),
                                                    LogicOp.OR,
                                                    implFormula_.getThenFormula());
            replacement = (Formula)replacement.applyReturnVisitor(this);
            replacement.annotateReplacing("", implFormula_);
            return replacement;                                            
        } else {
            return absorbNegation(implFormula_);
        }
    }

    public Object visit(QuantifiedExpr quantExpr_) {
        return absorbNegation(quantExpr_);
    }

    public Object visit(QuantifiedFormula quantForm_) {
        Quantifier quant = quantForm_.getQuantifier();
        if (!_skolemInsideUniv) {
            if (negateFormula() && quant.equals(Quantifier.SOME)) {
                // just switch it to an all and negate the body
                NegFormula nf = new NegFormula(quantForm_.getFormula());
                nf.annotateReplacing("", quantForm_.getFormula());
                Quantifier q = Quantifier.ALL;
                QuantifiedFormula replacement = new QuantifiedFormula(q,
                                                                      quantForm_.getDecls(),
                                                                      nf, true);
                replacement.setLeafIdMap(quantForm_.getLeafIdMap());
                replacement.annotateReplacing("", quantForm_);
                return replacement;
            }
        }
        
            // first, convert the body
            // has the same effect as moving the
            // negation inside the quantifier
        if (_skolemInsideUniv || (negateFormula() && (quant.equals(Quantifier.ALL)))) {
            quantForm_.setFormula((Formula)quantForm_.getFormula().applyReturnVisitor(this));
        }
        if (negateFormula()) {
            // switch some to all and all to some
            Quantifier newQuant = (quant.equals(Quantifier.ALL))
            ? Quantifier.SOME
            : Quantifier.ALL;
            QuantifiedFormula replacement = new QuantifiedFormula(newQuant,
                                                                      quantForm_.getDecls(),
                                                                  quantForm_.getFormula(), true);
            replacement.setLeafIdMap(quantForm_.getLeafIdMap());
            replacement.annotateReplacing("", quantForm_);
            return replacement;
        }
        return quantForm_;
    }
                                   
    private boolean negateFormula() {
        return _negCount % 2 != 0;
    }

    /**
     * converts children, absorbing negation if necessary
     * and negating formula if necessary
     */
    private Formula absorbNegation(Formula formula_) {
        if (negateFormula()) {
            // absorb negation by temporarily incrementing neg count
            // NOTE: this is unnecessary if skolemization cannot be
            // done inside comprehension expressions
            _negCount++;
            visit((Node)formula_);
            _negCount--;
            NegFormula nf = new NegFormula((Formula)formula_.copy());
            nf.annotateReplacing("", formula_);
            return nf;
        } else {
            return (Formula)visit((Node)formula_);
        }
    }
}
